package sample.sat;

import java.util.ArrayList;

import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.IProblem;
import org.sat4j.specs.ISolver;

public class SATSample {
	public static void main(String[] args) throws Exception{
		final int MAXVAR = 4;
		final int NBCLAUSES = 8;
		
		int[][] clauses = {	{-1,2,4},
							{-2,3,4},
							{1,-3,4},
							{1,-2,-4},
							{2,-3,-4},
							{-1,3,-4},
							{1,2,3},
							{-1,-2,-3}
							};
		
		ISolver solver = SolverFactory.newDefault();

		// prepare the solver to accept MAXVAR variables. MANDATORY for MAXSAT solving
		solver.newVar(MAXVAR);
		solver.setExpectedNumberOfClauses(NBCLAUSES);
		// Feed the solver using Dimacs format, using arrays of int
		// (best option to avoid dependencies on SAT4J IVecInt)
		for (int i=0;i<NBCLAUSES;i++) {
		  //int [] clause = {1, -3, 7};// get the clause from somewhere
		  // the clause should not contain a 0, only integer (positive or negative)
		  // with absolute values less or equal to MAXVAR
		  // e.g. int [] clause = {1, -3, 7}; is fine
		  // while int [] clause = {1, -3, 7, 0}; is not fine
			int[] clause = clauses[i];
			solver.addClause(new VecInt(clause)); // adapt Array to IVecInt
		}

		// we are done. Working now on the IProblem interface
		IProblem problem = solver;
		if (problem.isSatisfiable()) {
			System.out.println("shut the fuck up!");
			int[] model = problem.model();
			for(int i : model){
				System.out.print(i+",");
			}
			System.out.println("\n"+problem.isSatisfiable());
		} else {
			System.out.println("smack your bitch up!");
			
			ArrayList<String> temp = new ArrayList<String>();
			String className = temp.getClass().getName();
			System.out.println(className);
			Object b = Class.forName(className).newInstance();
			System.out.println("b is " + b.getClass().getName());
		}
	}
	
}
